The present application is related to the following co-pending U.S. patent applications, incorporated herein by reference in their entirety:
Ser. No. 11/086,721, filed Mar. 22, 2005 and entitled “Method And System For Reduction Of And/Or Subexpressions In Structural Design Representations;”
Ser. No. 11/086,720, filed Mar. 22, 2005 and entitled “Method And System For Reduction Of XOR/XNOR Subexpressions In Structural Design Representations.”
1. Technical Field
The present invention relates in general to verifying designs and in particular to reducing resource consumption during verification. Still more particularly, the present invention relates to a system, method and computer program product for performing verification by closely coupling rewriting algorithms and a structural satisfiability solver.
2. Description of the Related Art
With the increasing penetration of processor-based systems into every facet of human activity, demands have increased on the processor and application-specific integrated circuit (ASIC) development and production community to produce systems that are free from design flaws. Circuit products, including microprocessors, digital signal and other special-purpose processors, and ASICs, have become involved in the performance of a vast array of critical functions, and the involvement of microprocessors in the important tasks of daily life has heightened the expectation of error-free and flaw-free design. Whether the impact of errors in design would be measured in human lives or in mere dollars and cents, consumers of circuit products have lost tolerance for results polluted by design errors. Consumers will not tolerate, by way of example, miscalculations on the floor of the stock exchange, in the medical devices that support human life, or in the computers that control their automobiles. All of these activities represent areas where the need for reliable circuit results has risen to a mission-critical concern.
In response to the increasing need for reliable, error-free designs, the processor and ASIC design and development community has developed rigorous, if incredibly expensive, methods for testing and verification for demonstrating the correctness of a design. The task of hardware verification has become one of the most important and time-consuming aspects of the design process.
Among the available verification techniques, formal and semiformal verification techniques are powerful tools for the construction of correct logic designs. Formal and semiformal verification techniques offer the opportunity to expose some of the probabilistically uncommon scenarios that may result in a functional design failure, and frequently offer the opportunity to prove that the design is correct (i.e., that no failing scenario exists).
Unfortunately, the resources needed for formal verification, or any verification, of designs are proportional to design size. Formal verification techniques require computational resources which are exponential with respect to the design under test. Simulation scales polynomially and emulators are gated in their capacity by design size and maximum logic depth. Semi-formal verification techniques leverage formal algorithms on larger designs by applying them only in a resource-bounded manner, though at the expense of incomplete verification coverage. Generally, coverage decreases as design size increases.
Many tasks in computer-aided design (CAD), such as equivalence checking, property checking, logic synthesis, timing analysis, and false-path analysis, require Boolean reasoning on problems derived from circuit structures. The two main approaches used for such applications are Binary Decision Diagrams (BDDs) and Satisfiability (SAT) solving. The former converts the problem into a functionally canonical form, while the latter systematically searches for a consistent assignment of values for the variables of the problem. Typically, SAT solvers are based on the Davis-Putnam procedure that attempts to find a consistent assignment using a branch-and-bound approach. Unsatisfiability is proven if the SAT solver exhaustively enumerates all possible cases without finding a satisfying assignment.
As described in U.S. Pat. No. 6,473,884 B1 (Method and System for Equivalence-Checking Combinational Circuits Using Iterative Binary-Decision-Diagram Sweeping and Structural Satisfiability Analysis), which is incorporated herein by reference in its entirety, BDD sweeping and structural SAT algorithms are applied in an interleaved manner on a shared graph representation of the circuit. Such an intertwined application of these techniques results in a powerful summation of their orthogonal strengths. BDDs work very well if the redundancy of the problem structure eludes an exponential growth during construction. Structural SAT is efficient if the underlying circuit structure can be exploited for effective local search heuristics. In a synergistic setting, an interleaved application of BDD sweeping incrementally reduces the search space for the SAT solver until the problem is solved. The referenced patent focuses on equivalence checking, but this technique can be easily extended to other applications requiring Boolean reasoning such as property checking and false paths analysis.
Unfortunately, prior art systems for multi-algorithmic SAT solving lack the ability to closely integrate the use of closely-integrated rewriting tools to further compact the netlist in an attempt to reduce the search space for the SAT-solver in dimensions qualitatively beyond those possible by mere BDD sweeping, or more generally redundancy removal, alone.